Binary Decision Trees.html (2566B)
1 <?xml version="1.0" encoding="UTF-8"?> 2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> 3 <html><head><link rel="stylesheet" type="text/css" href="sitewide.css"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/><meta name="exporter-version" content="Evernote Mac 7.0.3 (456341)"/><meta name="keywords" content="logic"/><meta name="altitude" content="-0.7498652935028076"/><meta name="author" content="Alex Balgavy"/><meta name="created" content="2018-03-06 14:33:04 +0000"/><meta name="latitude" content="52.33306697436191"/><meta name="longitude" content="4.865391302397034"/><meta name="source" content="desktop.mac"/><meta name="updated" content="2018-03-27 15:56:25 +0000"/><title>Binary Decision Trees</title></head><body><div><b>Binary Decision Trees</b></div><div>used to represent a boolean function</div><div>dashed line to left is 0, solid line to right is 1</div><div>a formula is satisfiable if there is at least 1 leaf with a 1</div><div><br/></div><div><div><img src="Binary%20Decision%20Trees.resources/screenshot.png" height="166" width="443"/><br/></div></div><div><br/></div><div><br/></div><div><span style="font-weight: bold;">Ordered Binary Decision Diagram (OBDD)</span></div><div>collapsing and removing nodes in a binary decision tree</div><div><br/></div><div>rules:</div><div><ol><li>leaves with 0 and 1 are collapsed</li><li>repeat:</li><ul><li>if 0 and 1 edge of non-leaf n lead to same node m:</li><ul><li>eliminate n</li><li>redirect its incoming edges to m</li></ul><li>if non-leaves associated with same bool variable have 0 edge to same node and 1 edge to same node, then collapse</li></ul></ol><div><br/></div></div><div>non-isomorphic reduced OBDDs are never semantically equivalent</div><div>sensitive to order change (which nodes are above which)</div><div><br/></div><div>logical operations:</div><div><ul><li>negation — swap 0 and 1 in leaf nodes</li><li>disjunction:</li><ul><li>leaves: O2 if O1 is 0, otherwise O1</li><li>non-leaves: draw new nodes with disjunctions of previous Os</li></ul></ul></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;"><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;"><div><img src="Binary%20Decision%20Trees.resources/screenshot_1.png" height="199" width="656"/><br/></div></blockquote></blockquote><div><ul><li>conjunction:</li><ul><li>leaves: O2 if O1 is 1, otherwise O1</li><li>non-leaves: same as disjunction</li></ul></ul></div><div><br/></div></body></html>